(set-logic QF_LRA)
(declare-fun x () Bool)
(declare-fun y () Bool)
(declare-fun z () Bool)
(declare-fun a () Bool)
(assert (or y x))
(assert (or a z))
(push 1)
(assert (or y (not x)))
(assert (or (not a) z))
(push 1)
(assert (or (not z) (not y)))
(check-sat)
(pop 1)
(assert true)
(check-sat)
(pop 1)
(assert (or z y))
(assert (or (not z) y))
(assert (or (not y) (not a)))
(assert (or (not y) (not z)))
(check-sat)
